Termination w.r.t. Q proof of TRS/secret05cime1.trs

Termination w.r.t. Q of the following Term Rewriting System could not be shown:

Q restricted rewrite system:
The TRS R consists of the following rules:

sortSu(circ(sortSu(cons(te(a), sortSu(s))), sortSu(t))) → sortSu(cons(te(msubst(te(a), sortSu(t))), sortSu(circ(sortSu(s), sortSu(t)))))
sortSu(circ(sortSu(cons(sop(lift), sortSu(s))), sortSu(cons(te(a), sortSu(t))))) → sortSu(cons(te(a), sortSu(circ(sortSu(s), sortSu(t)))))
sortSu(circ(sortSu(cons(sop(lift), sortSu(s))), sortSu(cons(sop(lift), sortSu(t))))) → sortSu(cons(sop(lift), sortSu(circ(sortSu(s), sortSu(t)))))
sortSu(circ(sortSu(circ(sortSu(s), sortSu(t))), sortSu(u))) → sortSu(circ(sortSu(s), sortSu(circ(sortSu(t), sortSu(u)))))
sortSu(circ(sortSu(s), sortSu(id))) → sortSu(s)
sortSu(circ(sortSu(id), sortSu(s))) → sortSu(s)
sortSu(circ(sortSu(cons(sop(lift), sortSu(s))), sortSu(circ(sortSu(cons(sop(lift), sortSu(t))), sortSu(u))))) → sortSu(circ(sortSu(cons(sop(lift), sortSu(circ(sortSu(s), sortSu(t))))), sortSu(u)))
te(subst(te(a), sortSu(id))) → te(a)
te(msubst(te(a), sortSu(id))) → te(a)
te(msubst(te(msubst(te(a), sortSu(s))), sortSu(t))) → te(msubst(te(a), sortSu(circ(sortSu(s), sortSu(t)))))

Q is empty.

↳ QTRS

Q restricted rewrite system:
The TRS R consists of the following rules:

sortSu(circ(sortSu(cons(te(a), sortSu(s))), sortSu(t))) → sortSu(cons(te(msubst(te(a), sortSu(t))), sortSu(circ(sortSu(s), sortSu(t)))))
sortSu(circ(sortSu(cons(sop(lift), sortSu(s))), sortSu(cons(te(a), sortSu(t))))) → sortSu(cons(te(a), sortSu(circ(sortSu(s), sortSu(t)))))
sortSu(circ(sortSu(cons(sop(lift), sortSu(s))), sortSu(cons(sop(lift), sortSu(t))))) → sortSu(cons(sop(lift), sortSu(circ(sortSu(s), sortSu(t)))))
sortSu(circ(sortSu(circ(sortSu(s), sortSu(t))), sortSu(u))) → sortSu(circ(sortSu(s), sortSu(circ(sortSu(t), sortSu(u)))))
sortSu(circ(sortSu(s), sortSu(id))) → sortSu(s)
sortSu(circ(sortSu(id), sortSu(s))) → sortSu(s)
sortSu(circ(sortSu(cons(sop(lift), sortSu(s))), sortSu(circ(sortSu(cons(sop(lift), sortSu(t))), sortSu(u))))) → sortSu(circ(sortSu(cons(sop(lift), sortSu(circ(sortSu(s), sortSu(t))))), sortSu(u)))
te(subst(te(a), sortSu(id))) → te(a)
te(msubst(te(a), sortSu(id))) → te(a)
te(msubst(te(msubst(te(a), sortSu(s))), sortSu(t))) → te(msubst(te(a), sortSu(circ(sortSu(s), sortSu(t)))))

Q is empty.